Inference at * 
Iof proof for Lemma wellfounded functionality wrt iff:


  T1,T2:Type, r1:(T1T1), r2:(T2T2).
  (T1 = T2)
   (x,y:T1. r1(x,y)  r2(x,y))
   (WellFnd{i}(T1;x,y.r1(x,y))  WellFnd{i}(T2;x,y.r2(x,y))) 

latex

 by ((UnivCD) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 1. T1 : Type
C1: 2. T2 : Type
C1: 3. r1 : T1T1
C1: 4. r2 : T2T2
C1: 5. T1 = T2
C1: 6. x,y:T1. r1(x,y)  r2(x,y)
C1:   WellFnd{i}(T1;x,y.r1(x,y))  WellFnd{i}(T2;x,y.r2(x,y))
C.

Definitions	P  Q, P  Q, t  T, x(s1,s2), P  Q, P  Q, , x:A. B(x)
Lemmas	iff wf